$\forall$$T$:Type, $R$, ${\it R'}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$, $y$:$T$. \{$R$($x$,$y$) $\Rightarrow$ ${\it R'}$($x$,$y$)\}) $\Rightarrow$ \{Connex($T$;$x$,$y$.$R$($x$,$y$)) $\Rightarrow$ Connex($T$;$x$,$y$.${\it R'}$($x$,$y$))\}